\documentclass[12pt,a4paper,oneside,final]{book}
\usepackage[utf8]{inputenc}
\usepackage[IL2]{fontenc}
\usepackage[czech]{babel}
%\usepackage{mathptmx}
\usepackage{longtable}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{amsfonts}



\theoremstyle{plain}
\newtheorem{veta}{Věta}[section]
\newtheorem{lemma}[veta]{Lemma}

\theoremstyle{definition}
\newtheorem{definice}[veta]{Definice}
\newtheorem{pozn}[veta]{Poznámka}


\begin{document}
\chapter*{Úvod}
V dnešní době moderní matematiky převládá snaha zkoumat problémy v co možná nejobecnější formě. Zvlášť obory, jako je algebra, kombinatorika, nebo teoretická informatika, jsou vystavěny na abstraktních pojmech a definicích a člověk potom jen těžko pozná, na jaké konkrétní problémy se daná teorie vztahuje, nebo jaké má aplikace. Tento problém se však netýká pouze přímého využití v praxi. Velice často se zjišťuje, že dva pojmy, které spolu nemají zdánlivě mnoho společného, dávají dohromady velice zajímavé a důležité výsledky, kterých by se jinak dosahovalo velice složitě. Jedním s těchto případů je využití relace dobré předuspořádání v teorii formálních jazyků. 

Jedním z hlavních problémů zkoumaných v teorii formální jazyků je otázka, za jakých podmínek je daný jazyk regulární. Regulární jazyk je definován jako množina popsaná nějakým regulárním výrazem, regulární gramatikou nebo konečným automatem. Spojitost těchto pojmů se vysvětluje v základních kurzech formálních jazyků. Ukazuje se tak výhoda, kterou je zkoumaní jednoho pojmu pomocí různých přístupů. Regulární jazyky mají mnoho zajimavých vlastností, jako je například uzavřenost na množinové booleovské operace, zřetězení, Kleeneho hvězdičku nebo homomorfismy. Co se však může zdát jako složitý problém, má mnohdy jednoduché řešení při využití jiného přístupu. 

Jedním ze základních výsledků formálních jazyků je Nerodova věta, která popisuje regulární jazyky jako množiny vyplněné třídami nějaké kongruence (monotónní ekvivalence) konečného indexu. Tento výsledek je vlastě snaha o algebraický popis faktu, že je daný jazyk rozpoznáván konečným automatem. Třídy ekvivalentních slov totiž odpovídají stavům daného automatu. Tento výsledek se dá ovšem zobecnit a místo relace ekvivalence se uvažuje obecnější relace předuspořádání. Ukazuje se, že v případě předuspořádání se podmínka na konečnost dá nahradit slabší podmínkou, aby předuspořádání bylo dobré. 

Dalším z formalismů studovaných teorií formálních jazyků jsou přepisovací systémy, anglicky někdy označované jako semi-Thue systems. Ty indukují na množině všech slov předuspořádání a nabízí proto otázka, za jakých podmínek je toto předuspořádání dobré. V takových případech jsou jazyky uzavřené na tento přepisovací systém regulární. Ukážeme si několik tříd přepisovacích systémů, které tuto podmínku splňují.

Na závěr této práce si ukážeme, jak se dájí popsané výsledky využít při řešení nerovnic, ve kterých jsou konstanty i proměnné jazyky.




\chapter{Připomenutí pojmů}

emph{Jazyk L} nad abecedou $\Sigma$ je libovolná podmnožina $\Sigma^*$, tj. libovolná množina slov nad abecedou $\Sigma$. 

Mějme jazyky $L, K /subseteq \Sigma^*$. Vzhledem k tomu, že $L$ i $K$ jsou množiny, můžeme na ně aplikovat obvyklé operace \emph{sjednocení, průnik} a \emph{komplement}. Navíc si definujeme operace \emph{zřetězení, iteace} a \emph{pozitivní iterace}.

\[\text{Zřetězení            }		L \cdot K = \{uv | \: u\in L a v \in K\}\] 
\[\text{Iterace            }		L^*  = \{u_1 \cdots u_n | \: 0\leq n a u_1, \cdots, u_n \in L\}\] 
\[\text{Pozitivní iterace            }		L^+  = \{u_1 \cdots u_n | \: 0< n a u_1, \cdots, u_n \in L\}\] 

\begin{definice}
Nechť $\Sigma$ je abeceda. Třídu regulárních jazyků nad abecedou $\Sigma$ definujeme induktivně takto:
\begin{enumerate}
  \item[1.]Množiny {\o} a {a} pro každé $a \in \Sigma$ jsou regulárnní jazyky nad abecedou $\Sigma$.
  \item[2.]Jsou-li $L, K \subseteq \Sigma^*$ regulární, pak jsou také $L \cup K, L\ cdot K, L^*$ regulární jazyky nad $\Sigma$.
  \item[3.]Každý regulární jazyk nad abecedou $\Sigma$ vznikne po konečném počtu aplikací kroků 1. a 2.
\end{enumerate} 

\end{definice}

\begin{definice}
\label{monotonie}
  Nechť $\Sigma$ je abeceda a $\rho$ binární relace na množině $\Sigma^*$.
  Řekneme, že $\rho$ je \emph{monotónní}, pokud pro každé $x_1, x_2, y_1, y_2 \in \Sigma^*$ platí:
  \[x_1 \: \rho \: y_1, \: x_2 \: \rho \: y_2   \Rightarrow x_1 x_2 \: \rho \: y_1 y_2       \]
  Řekneme, že $\rho$ je zprava (zleva) \emph{monotónní}, pokud pro každé $x_1, x_2, y \in \Sigma^*$ platí:
   \[x_1 \: \rho \: x_2,  \Rightarrow x_1 y \: \rho \: x_2 y \;\;\; (y x_1 \: \rho \: y x_2)      \]
  Relace ekvivalence $\sim$ na množine $\Sigma^*$, která je (zprava) monotónní se nazývá (pravá) \emph{kongruence}.
\end{definice}   

Následující věta jinak známá jako Nerodova dává základní algebraickou charakterizaci regulárních jazyků.

\begin{veta}
\label{nerode}
  Nechť $L\subseteq\Sigma^*$. Potom $L$ je regulární právě tehdy, když je sjednocením některých tříd pravé kongruence na $\Sigma^*$ konečného indexu.
\end{veta}

  Abychom na základě předchozího tvrzení mohli o některém jazyku $L$ tvrdit, že je regulární,
  stačí nám nalézt vhodnou kongruenci konečného indexu a ukázat, že daný jazyk je vyplněn nekterými
  třídami ekvivalence. Pokud bychom však chtěli tvrdit opak, tedy že $L$ není regulární, stáli bychom před nelehkým úkolem.
  Museli bychom ukázat, že žádná kongruence požadovaných vlastností neexistuje.  
  Tento problém řeší silnější tvrzení, tzv. Myhill-Nerodova věta, která se opírá o pojem kontextu.

\begin{definice}
\label{kontext}
  Nechť $L\subseteq\Sigma^*$ je jazyk (ne nutně regulární). Potom pro libovolné $x\in\Sigma^*$ definujme množinu \emph{kontextů} prvku $x$ v jazyce $L$ takto:
  \[C_L(x)=\{(y,z)\mid y,z \in \Sigma^*, yxz \in L\}.\]
Dále definujme pravý a levý kontext (prefix, suffix) následovně:
  \[C_L^r(x)=\{y \in \Sigma^*, xy \in L\},\]
  \[C_L^l(x)=\{y \in \Sigma^*, yx \in L\}.\]
Na základě pravého kontextu můžeme nyní zadefinovat relaci $\sim_L^r$ :
  \[x\sim_L^r y  \Longleftrightarrow C_L^r(x) = C_L^r(y).\]
\end{definice}  

Relaci $\sim_L^r$ se říká \emph{pravá syntaktická ekvivalence} a je zřejmé, že jde o pravou kongruenci.
Relace $\sim_L^r$ má tu vlastnost, že pro libovolný jazyk $L$ platí, že je sjednocením některých
tříd $\Sigma^*/_{\sim_L^r}$. 

\begin{lemma}
Nechť $L\subseteq\Sigma^*$. Potom $L$ je sjednocením některých tříd rozkladu  $\Sigma^*/_{\sim_L^r}$.
\end{lemma}

\begin{proof}
Chceme dokázat, že pro libovolné $x \in \Sigma^*$ patří třída $[x]_{\sim_L^r}$ buď celá do $L$, nebo s ním má prázdný průnik. Nechť tedy $y$ je libovolné slovo takové, že $x\sim_L^r y$. Potom podle definice platí  $C_L^r(x) = C_L^r(y)$, neboli $xz \in L \Longleftrightarrow yz \in L$. Zvolme tedy $z=\epsilon$ a dostaneme $x \in L \Longleftrightarrow y \in L$.
\end{proof}

Další zajímavou vlastností je, že každá pravá kongruence, pro kterou platí, že je jazyk
$L$ sjednocením jejích tříd ekvivalence, je zjemněním relace $\sim_L^r$. Je tedy ze všech takových kongruencí největší.
Tato vlastnost je formálně shrnuta v následujícím lemmatu. 

\begin{lemma}
  Nechť $L\subseteq\Sigma^*$ a $\sim$ je libovolná pravá kongruence na množině $\Sigma^*$ taková, že $L$ je sjednocením některých tříd rozkladu. Potom platí, že $\sim ~\subseteq ~ \sim_L^r$. 
\end{lemma}
\begin{proof}
Dokážeme, že pro libovolná slova $x, y$ taková, že platí $x \sim y$ , platí také $x \sim_L^r y$. Relace $\sim$ je pravá kongruence, a proto platí  $xz \sim yz$ pro libovolné $z \in \Sigma^*$.
Protože $L$ je sjednocením některých tříd ekvivalence  $\sim$, platí $xz \in L \Longleftrightarrow yz \in L$. Tento vztah platí pro libovolné $z$, z toho vyplývá rovnost $C_L^r(x)=C_L^r(y)$ a tedy $x \sim_L^r y$.

\end{proof}

Z Nerodovy věty a předchozího tvrzení už přímo plyne Myhill-Nerodova věta.
 
\begin{veta}
\label{Myhill-Nerode}
  Nechť $L\subseteq\Sigma^*$. Potom jsou následující tvrzení ekvivalentní:
  \begin{enumerate}
    \item[(i)] L je regulární jazyk.
    \item[(ii)] Relace $\sim_L^r$ má konečný index.
  \end{enumerate}
\end{veta} 



Myhill-Nerodova věta je tedy podstatně silnější. Říká nám přesně na kterou
z pravých kongruencí se máme zaměřit. Navíc v případě, že má tato kongruence nekonečný 
index, nemůže být zkoumaný jazyk regulární. 

Předchozí věta nám dává nutnou i postačující
podmínku regularity jazyka a tedy úplnou charakterizaci. Zjistit, zda je
konkrétní jazyk regulární lze však více způsoby. Například sestrojením konečného automatu rozpoznávajícího daný jazyk, nebo pomocí
uzávěrových vlastností. My se zaměříme na některá zobecnění Myhill-Nerodovy věty.

Pro aplikaci Nerodovy věty bylo třeba nalézt pravou kongruenci (monotónní ekvivalenci) konečného indexu. Místo ekvivalence však můžeme uvažovat
obecnější relaci, a to předuspořádání.  

\begin{definice}
  Binární relace $\leq$ na množině $S$ se nazývá \emph{předuspořádání}, právě když je reflexivní a tranzitivní.

  Nechť $X \subseteq S$. Potom říkáme, že množina $X$ je \emph{nahoru uzavřená} vzhledem k $\leq$ ,
  pokud pro libovolné prvky $x \in X$ a $s \in S$ platí:
  \[x \leq s \Longrightarrow s \in X.\]
  Dále budeme nahoru uzavřené množiny nazývat pouze \emph{uzavřené}. 
  
  Relace ekvivalence $\sim$ na $S$ definovaná vztahem
    \[x \: \sim \: y  \Longleftrightarrow x  \: \leq \: y \; \text{a zároveň} \; y  \: \leq \: x      \]
  se nazývá \emph{jádro předuspořádání $\leq$}.   
\end{definice}

Věta \ref{Myhill-Nerode} se nyní přeformuluje do následujícího znění.

\begin{veta}
\label{Myhill-preorder}
  Nechť $L\subseteq\Sigma^*$. Potom $L$ je regulární právě tehdy, když je uzavřený vzhledem k nějakému 
  monotónnímu předuspořánaní množiny $\Sigma^*$, jehož jádro má konečný index.
\end{veta}

Jak je vidět, přechodem k předuspořádání jsme se nikam významně neposunuli. Věta se totiž stále odvolává na ekvivalenci konečného indexu.
Platí totiž, že je-li jazyk $L$ uzavřený vzhledem k monotónnímu předuspořádání $\leq$, jehož jádro má konečný index,
pak je $L$ sjednocením některých tříd jádra $\leq$. Věta \ref{Myhill-preorder} je tedy pouze přeformulovaná věta  \ref{Myhill-Nerode}.
Tento postup byl původně použit z jiných důvodů, monónní předuspořádání dávájí totiž jenmější klasifikaci regulárních jazyků.
Zajimavé je však zamyšlení, jestli nelze rozpoznávat regulární jazyky i předuspořádáními nekonečných indexů.
Hledaným zobecněním jsou dobrá předuspořádání, kterým se bude věnovat následující kapitola.

\chapter{Dobrá předuspořádání}
Zatímco většina výsledků v teorii konečných automatů a regulárních jazyků je konstruktivního charakteru ve smyslu, že stroje (automaty, turingovy stroje) a výrazy jsou dány efektivně, občas se vyskytne výsledek, který je naprosto nekonstruktivní. Jako příklad je známá Hainesova věta. Řekneme, že slovo y je nadřetězcem slova x, pokud posloupnost písmen y obsahuje posloupnost písmen x.

V této kapitole se zaměříme na pojem \emph{dobré předuspořádání}. 
Nejprve zadefinujeme potřebné pojmy a následně si  ukážeme vztah 
dobrých předuspořádí s regulárními jazyky. Ve zbytku kapitoly si popíšeme několik způsobů jak dokázat, že předuspořádání je dobré.


Dobré předuspořádání je reflexivní a tranzitivní relace (předuspořádání),
pro kterou platí, že každá podmnožina obsahuje alespoň jeden minimální prvek a nejvýše 
konečně mnoho takových, které nejsou vzájemně ekvivalentní. 

Jde o zobecnění pojmu \emph{dobrého uspořádání} 
a tento popis se definici dobrého uspořádání nejvíce blíží. Existuje však více zbůsobů jak definovat dobré předuspořádání, z nichž několik uvedeme
 v následující definici. 
 
\begin{definice} 
\label{wqo}
 Předuspořádání $\leq$ na množině $S$ je \emph{dobré předuspořádání} právě tehdy, když platí jedno z následujících:

\begin{enumerate}
  \item[(i)] Každá podmnožina $X \subseteq  S$ obsahuje konečnou podmnožinu $Y\subseteq X$ takovou, 
  že
  \[ \forall x \in X \  \exists y \in Y : y \le x.\]
  \item[(ii)] V libovolné posloupnosti $\{ x_i \}_{i=1}^\infty $ existují $i,j \in \mathbb{N}, i < j$ taková,
   že platí $x_i \leq x_j.$ 
  \item[(iii)] Libovolná nekonečná posloupnost prvků z $S$ obsahuje nekonečnou rostoucí podposloupnost.
  \item[(iv)] Množina $S$ neobsahuje ostře klesající nekonečnou posloupnost ani nekonečnou posloupnost vzájemně neporovnatelných prvků.
  \item[(v)] Libovolná posloupnost uzavřených podmnožin $S$, která je ostře rostoucí vzhledem k inkluzi, je konečná.
\end{enumerate}
\end{definice}

Lze jednoduše ověřit, že všech pět definic je ekvivalentních.
První z podmínek se nazývá \emph{vlastnost konečné báze}. Každá uzavřená množina $X$ totiž obsahuje konečnou podmnožinu, jejímž uzávěrem je 
právě množina $X$, která je tak konečně generovaná.Při rozpoznávání jazyků monotónními předuspořádáními nám k regularitě místo konečného indexu stačí vlastnost konečné báze, jak vyplyne z důkazu následující věty.
Důkaz samotný je převzat z ??.


\begin{veta}
\label{genMyh}
Nechť $L\subseteq\Sigma^*$. Potom $L$ je regulární právě tehdy, když je uzavřený vzhledem k nějakému 
monotónnímu dobrému předuspořánaní množiny $\Sigma^*$.
\end{veta}

\begin{proof}


Je jednoduché si uvědomit, že každé předuspořádání konečného indexu je dobré. Stačí nám tedy ukázat, že podmnožiny množiny $\Sigma^*$ uzavřené
vzhledem k monotónnímu dobrému předuspořádání jsou regulární. Důkaz provedeme sporem. Předpokládejme tedy, že máme monotónní dobré předuspořádání $\leq$ na množině
$\Sigma^*$ a množinu $L$ uzavřenou vzhledem k $\leq$, která není regulární. Z věty \ref{Myhill-Nerode} plyne, že relace $\sim_L$ má nekonečný index,
můžeme proto sestrojit nekonečnou posloupnost vzájemně neekvivalentních slov $\{x_i\}_{i=1}^\infty$. Podle definice \ref{wqo} můžeme z posloupnosti $\{x_i\}_{i=1}^\infty$
vybrat rostoucí podposloupnost vzhledem k $\leq$. Můžeme tedy předpokládat, že už samotná posloupnost $\{x_i\}_{i=1}^\infty$ byla vybrána jako rostoucí.
Z monotónie dostáváme, že pro libovolné $y \in \Sigma^*$ a $i < j $ platí $x_i y \leq x_j y$ a z uzavřenosti množiny $X$ plyne, že 
$x_i y \in L \Longrightarrow x_j y \in L $. Proto platí, že posloupnost pravých kontextů $\{C_L^r(x_i)\}_{i=1}^\infty$ je rostoucí vzhledem k inkluzi, a to dokonce ostře, 
neboť slova $x_i$ nejsou vzájemně ekvivalentní. Dále pro libovoná slova $y_1, y_2 \in \Sigma^*$ taková, že $y_1 \leq y_2$, platí $x_i y_1 \in L \Longrightarrow x_i y_2 \in L $.
Jsou tedy množiny $C_L^r(x_i)$  rovněž uzavřené vzhledem k  $\leq$. Posloupnost $\{C_L^r(x_i)\}_{i=1}^\infty$ je tedy nekonečná posloupnost uzavřených množin
ostře rostoucí vzhledem k inkluzi. Dostáváme spor, neboť podle definice \ref{wqo} části (v) takováto posloupnost není možná. Množina $L$ 
tedy musí být regulární.
 \end{proof}

V předchozím tvrzení jsme dostali zobecnění Nerodovy věty tím, že místo pravé kongruence jsme použili monotónní předuspořádání. V důkazu jsme využili monónnost z prava i zleva,
v případě kongruence nám však stačila pouze monotonie z prava. Jak se ukáže na příkladu, uzavřenost vzhledem k dobrému předuspořádání monotónnímu z prava k regularitě vést nemusít.

Příklad! ($\{ a^n b^m, kde \; n\leq m \}$)

Jednostranná monotonie tedy k regularitě nevede, věta \ref{genMyh} se přesto dá zobecnit. Stačí nalézt dvě dobrá předuspořádání $\leq_1 , \leq_2$, vzhledem k nimž bude jazyk $L$ uzavřený, přičemž $\leq_1$ je monotónní zprava
a $\leq_2$ zleva. 

\begin{veta}
\label{genMyh2}
Nechť $L\subseteq\Sigma^*$.  Potom $L$ je regulární právě tehdy, když je uzavřený vzhledem k nějakému 
 dobrému předuspořánaní  $\leq_1$ monotónnímu zprava a  dobrému předuspořánaní  $\leq_2$ monotónnímu zleva.

\end{veta}

K důkazu věty budeme potřebovat několik pojmů. Podobně jako jsme v definici \ref{kontext} definovali na základě kontextu syntaktickou kongruenci, si zadefinujeme \emph{syntaktické monotónní předuspořádání}.

\begin{definice}
Pro $L \subseteq\Sigma^* $ a prvky $x,y \in \Sigma^*$ definujeme relace:
  \[x\leq_L y  \Longleftrightarrow C_L(x) \subseteq C_L(y).\]
  \[x\leq_L^r y  \Longleftrightarrow C_L^r(x) \subseteq C_L^r(y).\]
  \[x\leq_L^l y  \Longleftrightarrow C_L^l(x) \subseteq C_L^l(y).\]
\end{definice}
Podobně jako v případě syntaktické kongruence se snadno ukáže, že syntaktické monotónní předuspořádání (resp. pravé/lévé) je největší monotónní předuspořádání, vzhledem k němuž je jazyk $L$ uzavřený.

\begin{lemma}
\label{monwqo}
 Nechť $L\subseteq\Sigma^*$ a $\leq$ je libovolné pravé (resp. levé) monotónní  předuspořádání na $\Sigma^*$, vzhledem ke kterému je jazyk $L$ uzavřený.  Potom platí, že $\leq \;\subseteq\; \leq_L^r$ (resp. $\leq \;\subseteq\; \leq_L^l$ ). 
\end{lemma}



\begin{proof}
Budeme dokazovat případ pro pravé monotńní předuspořádání.
Nechť  $x, y \in \Sigma^*$ jsou libovolná slova taková, že platí $x \leq y$. Z monotónnie $\leq$ plyne, že $xz \leq yz$ pro libovolné $z \in \Sigma^*$. 
Z uzavřenosti jazyka $L$ vzhledem k $\leq$ potom vyplývá, že $xz \in L \Longrightarrow yz \in L$ a tedy $ C_L^r(x) \subseteq C_L^r(y)$.

\end{proof}

Poslední vlastnost, kterou v důkazu věty \ref{genMyh2} využijeme, je, že se stačí zaměřit právě na předuspořádání $\leq_L^r$ a $\leq_L^l$. Najdeme-li totiž nějaká předuspořádání $\leq_1 , \leq_2$, která splňují podmínky věty \ref{genMyh2}, pak mají tuto vlastnost i $\leq_L^r$, $\leq_L^l$.

\begin{lemma}
\label{subwqo}
Nechť  $\leq_1$ je dobré předuspořádání a  $\leq_2$ je předuspořádání takové, že platí   $\leq_1\subseteq  \leq_2$. Potom je předuspořádání $\leq_2$ dobré.
\end{lemma}
\begin{proof}
K důkazu využijeme definici \ref{wqo}(ii). Pro  $\leq_1$ platí, že v libovolné posloupnosti $\{ x_i \}_{i=1}^\infty $ existují $i,j \in \mathbb{N}, i < j$ taková,
   že $x_i \leq_1 x_j$, tedy i   $x_i \leq_2 x_j$. Předuspořádání  $\leq_2$ je proto také dobré.
\end{proof}

\begin{proof}[Důkaz věty \ref{genMyh2}]
Je-li jazyk $L$ regulární, pak podle věty \ref{genMyh} víme, že je uzavřený vzhledem k dobrému předuspořádání, které je monotónní zprava i zleva. Opačnou implikaci budeme dokazovat sporem.
Nechť tedy $L$ není regulární. Potom podle věty \ref{Myhill-Nerode} má relace $\sim_L^r$ nekonečný index a existuje proto nekonečná posloupnost vzájemně neekvivalentních slov $\{x_i\}_{i=1}^\infty$. Podle předpokladu existují dobrá předuspořádání 
$\leq_1$ resp. $\leq_2$ monotónní zprava resp. zleva, vzhledem k nimž je $L$ uzavřený. Podle lemmat \ref{monwqo} a \ref{subwqo} mají tuto vlastnost také předuspořádání $\leq_L^r$, $\leq_L^l$. Z definice \ref{wqo}(ii) můžeme z posloupnosti $\{x_i\}_{i=1}^\infty$ vybrat podposloupnost $\{y_i\}_{i=1}^\infty$, která bude rostoucí vzhledem k předuspořádání $\leq_L^r$ a to dokonce ostře, neboť jsou $y_i$ vzájemně neekvivalentní v relaci $\sim_L^r$. Platí tedy, že 
$C_L^r(y_i) \subset C_L^r(y_{i+1})$ a posloupnost $\{C_L^r(y_i)\}_{i=1}^\infty$ je tedy ostře rostoucí vzhledem k inkluzi. Je zřejmé, že platí vztah $x\in C_L^r(y) \Longleftrightarrow y\in C_L^l(x) $. Z toho pro libovolná $z_1 \leq_L^l z_2$ plyne, že $z_1 \in C_L^r(y_i) \Longrightarrow y_i \in C_L^l(z_1) \subseteq C_L^l(z_2) \Longrightarrow z_2\in C_L^r(y_i)$.  Posloupnost $\{C_L^r(y_i)\}_{i=1}^\infty$ je pak posloupností uzavřených množin vzhledem k předuspořádání  $\leq_L^l$, která je ostře rostoucí vzhledem k inkluzi. To je ovšem spor s předpokladem, že předuspořádání  $\leq_L^l$ je dobré.
\end{proof}

\begin{veta}
Nechť $\leq$ je rozhodnutelné monotónní předuspořádání množiny $\Sigma^*$, pro které platí $u \leq v \Longrightarrow |u| \leq |v|$. Potom jsou následující podmínky ekvivalentní:

\begin{enumerate}
  \item[(i)]Všechny uzavřené jazyky vzhledem k $\leq$ jsou regulární.
  \item[(ii)]Všechny uzavřené jazyky vzhledem k $\leq$ jsou rekurzivní.
  \item[(iii)] $\leq$ je dobré předuspořádání.
\end{enumerate}
\end{veta}

\begin{lemma}
\label{soucinwqo}
Nechť $X$ je pologrupa předuspořádaná monotónní relací $\leq$ a $T_1, T_2 \subseteq X$. Pokud $\leq$ je dobré předuspořádání množin $T_1, T_2$, potom je dobré i na množině $T_1\cdot T_2$. 

\end{lemma}

Užitečným nástrojem pro dokázání, že dané předuspořádání je dobré, poskytuje věta, kterou poprvé dokázal Nash-Williams. K jejímu formulování potřebujeme definovat následující pojem.

\begin{definice}
Nechť $X$ je množina s předuspořádáním $\leq$ a $(x_i)_{i=1}^\infty$ je nekonečná posloupnost prvků množiny $X$. Posloupnost   $(x_i)_{i=1}^\infty$ nazveme \emph{špatnou}, právě když platí
\[  \forall i,j \in \mathbb{N} : i < j  \Longrightarrow x_i \not \leq x_j.\]
\end{definice}

Název \emph{špatná posloupnost} odpovídá tomu, že jsou to práve tyto posloupnosti, které nesmí obsahovat dobře předuspořádaná množina (\ref{wqo}(ii)).

\begin{definice}
Nechť $\leq$ je předuspořádání na množině $X$. Potom předuspořádání $\leq$ nazveme \emph{fundované}, právě když neexistuje nekočná posloupnost  $(x_i)_{i=1}^\infty, x_i \in X$, pro kterou platí $x_{i}>x_{i+1}, i \in \mathbb{N}$.
\end{definice}

Uveďme, že každé dobré předuspořádání je fundované, jak vyplývá z definice \ref{wqo}(iv).

Pro potřeby následující věty je nutné definovat lexikografické předuspořádání na nekonečných posloupnostech. Nechť $X$ je množina předuspořádaná relací $\leq$ a $\sim$ je její jádro. Definujme množinu nekonečných posloupností jako $X^{\omega}$. Potom předuspořádání $\leq$ indukuje předuspořádání na množině $X^{\omega}$ následujícím vztahem:
\[ (x_i)_{i=1}^\infty \leq  (y_i)_{i=1}^\infty \Longleftrightarrow \forall i \in \mathbb{N} : x_i \sim y_i \text{ nebo}\]
\[ \exists n : x_n \leq y_n \wedge \forall i<n : x_i \sim y_i     .\]

\begin{veta}

Nechť $\preceq$ je fundované předuspořádání na množině $X$. Nechť dále $\leq$ je předuspořádání na množině $X$, které není dobré. Potom existuje špatná posloupnost $(x_i)_{i=1}^\infty, x_i \in X$ vzhledem k předuspořádání $\leq$, která je minimální vzhledem k $\preceq$.

\end{veta}


\chapter{Přepisovací systémy}

V této kapitole si vysvětlíme pojem přepisovací systém a aplikuje dosavadní poznatky o vztahu regulárních jazyků s dobrými předuspořádáními. Přepisovací systémy mají stejnou vyjadřovací sílu jako Turingovy stroje. Nás bude zajímat, za jakých okolností jsou jazyky uzavřené vzhledem k danému přepisovacímu systému regulární. Ukáže se, že přepisovací systémy generují regulární jazyky právě když indukují dobré předuspořádání na slovech nad danou abecedou. Dále se zaměříme na  konkrétní třídy přepisovacích systémů a ukážeme, že indukují dobrá předuspořádání.

Přepisovací systémy

\begin{definice}
\emph{Přepisovací systém} je dvojice $(\Sigma, R)$, kde $\Sigma$ je abeceda a $R \subseteq \Sigma^* \times \Sigma^*$ je konečná množina dvojic slov, které se nazývají \emph{přepisovací pravidla}. Pravidlo $(u, v) \in R$ se také zapisuje $u \rightarrow v$, čímž se myslí, že slovo $u$ se přepíše na $v$. Relace $R$ se dá přirozeně rozšířít na další slova nad abecedou $\Sigma$ na relaci $\Rightarrow_R$  podle pravidla:
\[ x \Rightarrow_R y \Longleftrightarrow x=x_1 u x_2  \; \text{ a }  \; y = x_1 v x_2,  \: \text{kde}  \: x_1, x_2 \in \Sigma^*  \: \text{ a }  \: u \rightarrow v        .\]
Konečně reflexivní a tranzitivní uzávěr relace $\Rightarrow_R$ se značí $\Rightarrow_R^*$ a nazývá se \emph{relace odvození}.

\end{definice}

Pro libovolný přepisovací systém $(\Sigma, R)$ je tedy relace odvození $\Rightarrow_R^*$ předuspořádání na množině $\Sigma^*$. Vzhledem k definici relace $\Rightarrow_R^*$ je zřejmé, že je monotónní. Následuje základní tvrzení této kapitoly, které přímo vyplývá z věty \ref{genMyh}.

\begin{veta}
\label{Thue}
Nechť $(\Sigma, R)$ je přepisovací systém a $L$ je jazyk nad abecedou $\Sigma$ uzavřený vzhledem k relaci $\Rightarrow_R^*$. Potom $L$ je regulární, pokud relace $\Rightarrow_R^*$ je dobré předuspořádání. 
\end{veta}

Ve zbytku kapitoly se budeme zaobírat konkrétními  třídami přepisovacích systémů. 

\section{Unitární přepisovací systémy}
Jako první se zaměříme na unitární přepisovací systémy.

\begin{definice}
Nechť $\Sigma$ je konečná abeceda. Přepisovací systém $(\Sigma, R)$ nazveme \emph{unitární}, pokud množina jeho pravidel je ve tvaru 
\[R=\{\epsilon \rightarrow w | w\in I\},\]
kde $I \subseteq \Sigma^*$ je konečná množina slov. V tom případě je přepisovací systém jasně určen množinou $I$, budeme proto jím indukovanou relaci odvození značit $\Rightarrow_I^*$.
\end{definice}
Přepisování podle pravidel unitárního systému tedy znamená vkládání řetězců z množiny $I$. Je tedy zřejmé, že unitární přepisovací systémy generují bezkontextové jazyky. V našem zájmu bude zjistit, za jakých podmínek jsou jazyky uzavřené na relaci odvození regulární, tedy kdy je $\Rightarrow_I^* $ dobré předuspořádání. Jak se ukáže, musí mít množina $I$ vlastnost nevyhnutelnosti.

\begin{definice}
Nechť $I \subseteq \Sigma^* $. Potom množina $I$ je \emph{nevyhnutelná} (nad abecedou $\Sigma$), pokud existuje přirozené číslo $k_0$ takové, že libovolné slovo $u \in \Sigma^* $, pro které platí $|u|>k_0$, je ve tvaru $u = u_1wu_2$ pro $w \in I$ a $u_1, u_2 \in \Sigma^*$. Nejmenší $k_0$ s touto vlastností nazveme \emph{mez nevyhnutelnosti}.
\end{definice}

Nevyhnutelnost tedy znamená, že libovolné slovo delší než nějaká mez musí jako podřetězec obsahovat nějaké slovo z množiny $I$. Následující tvrzení dává nutnou i postačující podmínku k tomu, aby unitární přepisovací systém indukoval dobré předuspořádání.

\begin{veta}
\label{unitar}
Nechť $(\Sigma, R)$ je unitární přepisovací systém spolu s množinou $I$. Potom relace odvození $\Rightarrow_I^*$ je dobré předuspořádání právě tehdy, když je množina $I$ nevyhnutelná.
\end{veta}

K důkazu předchozí vety bude třeba nekolik pomocných tvrzení, jejihž důkazy lze najít například v ??.
Nejprve zadefinujeme posloupnost množin $(I_i)_{i=0}^\infty$ následovně:
\[I_0 = I^*, \: I_{n+1}=( \bigcup_{a_1, ... ,a_k \in \Sigma, a_1 \cdots  a_k \in I}I_n a_1 I_n a_2 \cdots  a_{k-1}I_n a_k i_n)^*\]

\

\begin{lemma}
\label{unitar1}
Pro libovolné $n\leq0$ je relace odvození $\Rightarrow_I^*$ dobré předuspořádání množiny $I_n$.
\end{lemma}
***
\begin{lemma}
\label{unitar2}
Pro libovolné $n\leq0$ platí:
\begin{enumerate}
  \item[(i)]Pokud $uv \in I_n \text{ a } w\in I, \text{ pak } uwv\in I_{n+1},$
  \item[(ii)]Pokud $uv \in I_n, |u|\leq |v| \text{ a } w\in I, \text{ pak } uwv\in I_{n+1},$
\end{enumerate}
\end{lemma}

Dále definujme pro libovolné $n\leq0$:
\[R(I_n)= \bigcup_{a_1, ... ,a_k \in \Sigma,k\leq n}I_n a_1 I_n a_2 \cdots  a_{k-1}I_n a_k I_n.\]

\begin{lemma}
\label{unitar3}
Nechť I je konečná nevyhnutelná podmnožina množiny $\Sigma^*$ a $k_0$ je mez nevyhnutelnosti $I$. Potom platí, že $\Sigma^* = R(I_k)$.
\end{lemma}

\begin{proof}[Důkaz v2ty \ref{unitar}]
Nevyhnutelnost množiny $I$ je zřejmě nutná podmínka. Aby byla relace $\Rightarrow_I^*$ dobré předuspořádání, nesmí podle definice \ref{wqo}(iv) existovat nekonečná posloupnost neporovnatelných prvků.  Platí-li však $u \Rightarrow_I^* w$, musí slovo $w$ obsahovat podslovo z  množiny $I$. Pokud tedy množina $I$ není nevyhnutelná, existuje nekonečná posloupnost slov neobsahujícíh podslova z množiny $I$ a jsou proto vzájemně neporovnatelná.

Nechť nyní $k_0$ je mez nevyhnutelnosti množiny $I$. Potom z lemmatu \ref{unitar3} vyplývá
\[ \Sigma^*= \bigcup_{a_1, ... ,a_k \in \Sigma,k\leq k_0}I_{k_0} a_1 I_{k_0} a_2 \cdots  a_{k-1}I_{k_0} a_k I_{k_0}. \]
Podle lemmatu \ref{unitar1} je $\Rightarrow_I^*$ dobré předuspořádání množiny $I_{k_0}$ a podle lammatu \ref{soucinwqo} také množiny $\Sigma^*$.

\end{proof}

\begin{pozn}
\label{nevyhnutelnost}
Podle věty \ref{unitar} umíme rozhodnout, zda daný unitární systém generuje regulární jazyky.To nastane v případě, že množina $I$ je nevyhnutelná. K tomu stačí ověřit, že množina slov, která neobsahují podslovo z množiny $I$, je konečná. Tuto množinu lze zapsat ve tvaru $\Sigma^* -\Sigma^*  I \Sigma^* $. Pro $I$ regulární jde o rozhodnutelny problém.
\end{pozn}

\section{OS schémata* }

V této časti se zaměříme na obecné bezkontextové přepisovací systémy. Konkrétně jsou to takové, ve kterých jsou všechna pravidla tvaru $a \rightarrow w$, kde $a \in \Sigma, w\in \Sigma^*$. 

\begin{veta}
Nechť $(\Sigma, R)$ je přepisovací systém, kde $R= \{a_i \rightarrow w_i | a_i \in \Sigma, w_i \in \Sigma^* , i=1, 2, ..., n\}$. Potom jsou následující podmínky ekvivalentní:

\begin{enumerate}
  \item[(i)] Relace odvození $\Rightarrow_R^*$ je dobré předuspořádání.
  \item[(ii)]$\{awa \: | a \in \Sigma, w\in \Sigma^*, a\Rightarrow_R^*awa\}$ je nevyhnutelná nad $\Sigma$.
  \item[(iii)]$\{aw \:| a \in \Sigma, w\in \Sigma^*, w \neq \epsilon, a\Rightarrow_R^*aw\}\: \cup \newline \{wa \:| a \in \Sigma, w\in \Sigma^*, w \neq \epsilon, a\Rightarrow_R^*wa\}$ je nevyhnutelná nad $\Sigma$.
\end{enumerate}
\end{veta}

Poznamenejme, že v tomto případě nejdou podmínky věty efektivně rozhodnout. Argument z poznámky \ref{nevyhnutelnost} nelze použít, neboť tyto množiny nejsou regulární.



\chapter{Definice LTL}
Ve čtvrté kapitole se nejprve seznámíme s lineární temporální logikou a ukážeme si, jak se tvoří její formule a jak pomocí těchto pojmů definovat jazyky. Dále se budeme zabývat fragmenty lineární temporální logiky, ve kterých se nevyskytuje žádné temporální operátory, nebo pouze jejich omezený počet. Na závěr si dokážeme dvě věty o uzávěrových vlastnostech třídy jazyků, jež jsou dány formulemi, v nichž se nevyskytuje žádný temporální operátor X. Podkladem pro tuto kapitolu byly převážně texty [12], [14], [22].

Připomeňme si nejprve standardní definici výrokové logiky, ze které budeme vycházet při definici lineární temporální logiky.

\begin{definice}
Mějme konečnou abecedu $A = \{a, b, c, ...\}$ písmen, závorky ( a ), logickou konstantu T a logické symboly $\vee , \neg$. Formule výrokové logiky se induktivně definuje pomocí následujících 4 pravidel:
\begin{enumerate}
  \item[(i)]T( true ) je formule,
  \item[(ii)]každé písmeno $a \in A$ je formule,
  \item[(iii)]jestliže $\phi$ je formule, pak i $(\neg \phi)$ je formule,
  \item[(iv)]jestliže $\phi$ a $\psi$ jsou formule, pak i $(\phi \vee \psi )$ je formule.
\end{enumerate} 
\end{definice} 


\end{document}




